\begin{tabbing}
$\forall$${\it the\_w}$:World, $e$:E.
\\[0ex]FairFifo
\\[0ex]$\Rightarrow$ ($\uparrow$isrcv(kind($e$)))
\\[0ex]$\Rightarrow$ ($\exists$\=$t$:\{0..time($e$)$^{-}$\}\+
\\[0ex](($\uparrow$match(lnk(kind($e$));$t$;time($e$)))
\\[0ex]\& (\=((0 $\leq$ ($\parallel$rcvs(lnk(kind($e$));time($e$))$\parallel$ {-} $\parallel$snds(lnk(kind($e$));$t$)$\parallel$))\+
\\[0ex]\& (\=($\parallel$rcvs(lnk(kind($e$));time($e$))$\parallel$ \+
\\[0ex]{-} $\parallel$snds(lnk(kind($e$));$t$)$\parallel$) $<$ $\parallel$onlnk\=(lnk(kind($e$))\+
\\[0ex];m(source(lnk(kind($e$)));$t$))$\parallel$))
\-\-\\[0ex]c$\wedge$ (\=onlnk(lnk(kind($e$));m(source(lnk(kind($e$)));$t$))[($\parallel$rcvs(lnk(kind($e$));time($e$))$\parallel$ \+
\\[0ex]{-} $\parallel$snds(lnk(kind($e$));$t$)$\parallel$)]
\\[0ex]=
\\[0ex]msg(a(loc($e$);time($e$)))
\\[0ex]$\in$ Msg))))
\-\-\-
\end{tabbing}